{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}

module U where

import TypeBasics (encode)
import TypeSums (inject)
import Yoko



data ULC = Lam ULC | Var Int
              | App ULC ULC deriving Show


data Lam_ = Lam_ ULC
data Var_ = Var_ Int
data App_ = App_ ULC ULC



type instance Range Lam_ = ULC
type instance Range Var_ = ULC
type instance Range App_ = ULC

type instance Tag Lam_ = $(return $ encode "Lam")
type instance Tag Var_ = $(return $ encode "Var")
type instance Tag App_ = $(return $ encode "App")

concat `fmap` mapM derive [''ULC, ''Lam_, ''Var_, ''App_]



type instance Rep Lam_ = Rec ULC
instance Generic Lam_ where
  rep (Lam_ tm) = Rec tm
  obj (Rec tm) = Lam_ tm
type instance Rep Var_ = Dep Int
instance Generic Var_ where
  rep (Var_ i) = Dep i
  obj (Dep i) = Var_ i
type instance Rep App_ = Rec ULC :*: Rec ULC
instance Generic App_ where
  rep (App_ tm1 tm2) = Rec tm1 :*: Rec tm2
  obj (Rec tm1 :*: Rec tm2) = App_ tm1 tm2





type instance DCs ULC =
  N Lam_ :+: N Var_ :+: N App_
instance DT ULC where
  disband (Lam tm)   = DCsOf . inject $ Lam_ tm
  disband (Var i)       = DCsOf . inject $ Var_ i
  disband (App tm1 tm2) = DCsOf . inject $ App_ tm1 tm2
instance DC Lam_ where rejoin (Lam_ tm)      = Lam tm
instance DC Var_ where rejoin (Var_ i)       = Var i
instance DC App_ where rejoin (App_ tm1 tm2) = App tm1 tm2
